MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: append#2(Cons(x8,x6),Cons(x2,x4)) -> Cons(x8,append#2(x6,Cons(x2,x4))) append#2(Nil(),Cons(x2,x4)) -> Cons(x2,x4) cond_partition_f_l_1(Pair(x23,x19),main_xs_1(x4),x2) -> ite_b#2(leqNat#2(x4,x2) ,Pair(x23,Cons(x2,x19)) ,Pair(Cons(x2,x23),x19)) cond_quicksort_gt_xyz_1(Pair(x3,x2),x1) -> append#2(quicksort#2(x3),Cons(x1,quicksort#2(x2))) ite_b#2(False(),Pair(x8,Cons(x10,x12)),Pair(Cons(x2,x4),x6)) -> Pair(Cons(x2,x4),x6) ite_b#2(True(),Pair(x8,Cons(x10,x12)),Pair(Cons(x2,x4),x6)) -> Pair(x8,Cons(x10,x12)) leqNat#2(x4,0()) -> True() leqNat#2(0(),S(x12)) -> False() leqNat#2(S(x4),S(x2)) -> leqNat#2(x4,x2) main(x1) -> quicksort#2(x1) partition#2(main_xs_1(x1),Nil()) -> Pair(Nil(),Nil()) partition#2(main_xs_1(x3),Cons(x2,x1)) -> cond_partition_f_l_1(partition#2(main_xs_1(x3),x1) ,main_xs_1(x3) ,x2) quicksort#2(Cons(x4,x6)) -> cond_quicksort_gt_xyz_1(partition#2(main_xs_1(x4),x6),x4) quicksort#2(Nil()) -> Nil() - Signature: {append#2/2,cond_partition_f_l_1/3,cond_quicksort_gt_xyz_1/2,ite_b#2/3,leqNat#2/2,main/1,partition#2/2 ,quicksort#2/1} / {0/0,Cons/2,False/0,Nil/0,Pair/2,S/1,True/0,main_xs_1/1} - Obligation: innermost runtime complexity wrt. defined symbols {append#2,cond_partition_f_l_1,cond_quicksort_gt_xyz_1 ,ite_b#2,leqNat#2,main,partition#2,quicksort#2} and constructors {0,Cons,False,Nil,Pair,S,True,main_xs_1} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE